enrich
   encoding-node-headerless
, 
   encoding-node-header
, 
   debug

with
   

   
   
   functions  . .flashsize : elem → nat;
              . .alignedsize : elem → nat;
   
   procedures encode_node# elem × nat : nat × buffer : error  nondeterministic;
              decode_node# nat × nat × buffer : elem : error  nondeterministic;
   variables  ND : elem flexible;
              BUF : buffer flexible;
              ISPAD : bool flexible;
              ispad : bool;
              NDHD : node-header flexible;
              NDSIZE : nat flexible;
              ALIGNEDSIZE : nat flexible;
              SIZE : nat flexible;
              OFFSET : nat flexible;
              SIZE0 : nat flexible;
              TRAILER : buffer flexible;
   
   

   

   axioms node-flash-size :  ⊦ nd.flashsize = 2 * NODE_HEADER_SIZE + nd.alignedsize;
          used for: s;
          alignedsize :  ⊦ nd.alignedsize = align↑(node-size-headerless(nd), 2 * NODE_HEADER_SIZE);

   

   declarations encode-node
                : encode_node#(ND, OFFSET; SIZE, BUF; ERR)
                  {let NDSIZE = node-size-headerless(ND)
                   in let ALIGNEDSIZE = align↑(NDSIZE, 2 * NODE_HEADER_SIZE), SIZE0 = ?
                      in {encode_header#(nodeheader(NDSIZE, false), OFFSET; BUF; ERR); 
                          if ERR = ESUCCESS then encode_node_headerless#(ND, OFFSET + NODE_HEADER_SIZE; BUF, SIZE0; ERR); 
                          if ERR = ESUCCESS
                          then {BUF := fill(BUF, empty, OFFSET + NODE_HEADER_SIZE + NDSIZE, ALIGNEDSIZE - NDSIZE); 
                                BUF := copy(validtrailer, 0, BUF, OFFSET + NODE_HEADER_SIZE + ALIGNEDSIZE, NODE_HEADER_SIZE)}; 
                          SIZE := 2 * NODE_HEADER_SIZE + ALIGNEDSIZE}
                  }
                ;
                decode-node
                : decode_node#(OFFSET, SIZE, BUF; ND; ERR)
                  {if SIZE < 2 * NODE_HEADER_SIZE
                   then {debug#("persistence: decode_node expected size wrong"); ERR := EINVAL}
                   else if ¬ OFFSET + SIZE ≤ # BUF
                        then {debug#("persistence: decode_node buffer insufficient"); ERR := EINVAL}
                        else let NDHD = ?
                             in {decode_header#(OFFSET, BUF; NDHD; ERR); 
                                 if ERR = ESUCCESS ∧ NDHD.ispadding then {debug#("persistence: decode_node got padding node"); ERR := EIO}; 
                                 if ERR = ESUCCESS ∧ align↑(NDHD.size, 2 * NODE_HEADER_SIZE) + 2 * NODE_HEADER_SIZE ≠ SIZE
                                 then {debug#("persistence: decode_node node of wrong size"); ERR := EIO}; 
                                 if ERR = ESUCCESS
                                 then {decode_node_headerless#(OFFSET + NODE_HEADER_SIZE, BUF; ND, SIZE; ERR); 
                                       if ERR ≠ ESUCCESS
                                       then debug#("persistence: decode_node decoding failed")
                                       else if SIZE ≠ NDHD.size then {debug#("persistence: decode_node size of node unexpected"); ERR := EINVAL}}; 
                                 if   ERR = ESUCCESS
                                    ∧ ¬
                                      range=
                                      (BUF, OFFSET + NODE_HEADER_SIZE + align↑(NDHD.size, 2 * NODE_HEADER_SIZE), validtrailer, 0, NODE_HEADER_SIZE)
                                 then {debug#("persistence: decode_node no validtrailer"); ERR := EIO}}
                  }
                ;
end enrich